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)

now :: thesis: for a being object st a in REAL 2 holds
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;

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