let OO, Ox, Oy be Element of REAL 2; :: thesis: ( OO = |[0,0]| & Ox = |[1,0]| & Oy = |[0,1]| implies REAL 2 = plane (OO,Ox,Oy) )

assume that

A1: OO = |[0,0]| and

A2: Ox = |[1,0]| and

A3: Oy = |[0,1]| ; :: thesis: REAL 2 = plane (OO,Ox,Oy)

hence REAL 2 = plane (OO,Ox,Oy) ; :: thesis: verum

assume that

A1: OO = |[0,0]| and

A2: Ox = |[1,0]| and

A3: Oy = |[0,1]| ; :: thesis: REAL 2 = plane (OO,Ox,Oy)

now :: thesis: for a being object st a in REAL 2 holds

a in plane (OO,Ox,Oy)

then
REAL 2 c= plane (OO,Ox,Oy)
;a in plane (OO,Ox,Oy)

let a be object ; :: thesis: ( a in REAL 2 implies a in plane (OO,Ox,Oy) )

assume a in REAL 2 ; :: thesis: a in plane (OO,Ox,Oy)

then reconsider b = a as Point of (TOP-REAL 2) by EUCLID:22;

A4: b = |[((b `1) + 0),(0 + (b `2))]| by EUCLID:53

.= |[((b `1) * 1),((b `1) * 0)]| + |[((b `2) * 0),((b `2) * 1)]| by EUCLID:56

.= ((b `1) * |[1,0]|) + |[((b `2) * 0),((b `2) * 1)]| by EUCLID:58

.= ((b `1) * |[1,0]|) + ((b `2) * |[0,1]|) by EUCLID:58 ;

reconsider a1 = 1 - ((b `1) + (b `2)) as Real ;

reconsider a2 = b `1 as Real ;

reconsider a3 = b `2 as Real ;

a1 * |[0,0]| = |[(a1 * 0),(a1 * 0)]| by EUCLID:58

.= |[0,0]| ;

then (a1 * |[0,0]|) + b = |[0,0]| + |[(b `1),(b `2)]| by EUCLID:53

.= |[(0 + (b `1)),(0 + (b `2))]| by EUCLID:56

.= b by EUCLID:53 ;

then A5: b = ((a1 * |[0,0]|) + (a2 * |[1,0]|)) + (a3 * |[0,1]|) by A4, RLVECT_1:def 3;

( (a1 + a2) + a3 = 1 & b = ((a1 * OO) + (a2 * Ox)) + (a3 * Oy) ) by A1, A2, A5, A3;

then a in { x where x is Element of REAL 2 : ex a1, a2, a3 being Real st

( (a1 + a2) + a3 = 1 & x = ((a1 * OO) + (a2 * Ox)) + (a3 * Oy) ) } ;

hence a in plane (OO,Ox,Oy) by EUCLIDLP:def 9; :: thesis: verum

end;assume a in REAL 2 ; :: thesis: a in plane (OO,Ox,Oy)

then reconsider b = a as Point of (TOP-REAL 2) by EUCLID:22;

A4: b = |[((b `1) + 0),(0 + (b `2))]| by EUCLID:53

.= |[((b `1) * 1),((b `1) * 0)]| + |[((b `2) * 0),((b `2) * 1)]| by EUCLID:56

.= ((b `1) * |[1,0]|) + |[((b `2) * 0),((b `2) * 1)]| by EUCLID:58

.= ((b `1) * |[1,0]|) + ((b `2) * |[0,1]|) by EUCLID:58 ;

reconsider a1 = 1 - ((b `1) + (b `2)) as Real ;

reconsider a2 = b `1 as Real ;

reconsider a3 = b `2 as Real ;

a1 * |[0,0]| = |[(a1 * 0),(a1 * 0)]| by EUCLID:58

.= |[0,0]| ;

then (a1 * |[0,0]|) + b = |[0,0]| + |[(b `1),(b `2)]| by EUCLID:53

.= |[(0 + (b `1)),(0 + (b `2))]| by EUCLID:56

.= b by EUCLID:53 ;

then A5: b = ((a1 * |[0,0]|) + (a2 * |[1,0]|)) + (a3 * |[0,1]|) by A4, RLVECT_1:def 3;

( (a1 + a2) + a3 = 1 & b = ((a1 * OO) + (a2 * Ox)) + (a3 * Oy) ) by A1, A2, A5, A3;

then a in { x where x is Element of REAL 2 : ex a1, a2, a3 being Real st

( (a1 + a2) + a3 = 1 & x = ((a1 * OO) + (a2 * Ox)) + (a3 * Oy) ) } ;

hence a in plane (OO,Ox,Oy) by EUCLIDLP:def 9; :: thesis: verum

hence REAL 2 = plane (OO,Ox,Oy) ; :: thesis: verum