Mathbox for Frédéric Liné < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-sside Unicode version

Definition df-sside 26163
 Description: Two points not on are on the same side of if the segment xy doesn't intersect . Definition 10 of [AitkenIBG] p. 4 (For my private use only. Don't use.) (Contributed by FL, 26-May-2016.)
Assertion
Ref Expression
df-sside ss Ibg PLines PPoints PPoints
Distinct variable group:   ,,,

Detailed syntax breakdown of Definition df-sside
StepHypRef Expression
1 csas 26162 . 2 ss
2 vg . . 3
3 cibg 26107 . . 3 Ibg
4 vl . . . 4
52cv 1622 . . . . 5
6 cplines 26058 . . . . 5 PLines
75, 6cfv 5255 . . . 4 PLines
8 vx . . . . . . . 8
98cv 1622 . . . . . . 7
10 cpoints 26056 . . . . . . . . 9 PPoints
115, 10cfv 5255 . . . . . . . 8 PPoints
124cv 1622 . . . . . . . 8
1311, 12cdif 3149 . . . . . . 7 PPoints
149, 13wcel 1684 . . . . . 6 PPoints
15 vy . . . . . . . 8
1615cv 1622 . . . . . . 7
1716, 13wcel 1684 . . . . . 6 PPoints
18 cseg 26130 . . . . . . . . . 10
195, 18cfv 5255 . . . . . . . . 9
209, 16, 19co 5858 . . . . . . . 8
2120, 12cin 3151 . . . . . . 7
22 c0 3455 . . . . . . 7
2321, 22wceq 1623 . . . . . 6
2414, 17, 23w3a 934 . . . . 5 PPoints PPoints
2524, 8, 15copab 4076 . . . 4 PPoints PPoints
264, 7, 25cmpt 4077 . . 3 PLines PPoints PPoints
272, 3, 26cmpt 4077 . 2 Ibg PLines PPoints PPoints
281, 27wceq 1623 1 ss Ibg PLines PPoints PPoints
 Colors of variables: wff set class This definition is referenced by:  isside0  26164
 Copyright terms: Public domain W3C validator