let S be non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct ; :: thesis: for a, b, c being POINT of S st not Collinear a,b,c holds
for E1, E2 being Subset of S st E1 is_plane & a in E1 & b in E1 & c in E1 & E2 is_plane & a in E2 & b in E2 & c in E2 holds
E1 = E2
let a, b, c be POINT of S; :: thesis: ( not Collinear a,b,c implies for E1, E2 being Subset of S st E1 is_plane & a in E1 & b in E1 & c in E1 & E2 is_plane & a in E2 & b in E2 & c in E2 holds
E1 = E2 )
assume A1: not Collinear a,b,c ; :: thesis: for E1, E2 being Subset of S st E1 is_plane & a in E1 & b in E1 & c in E1 & E2 is_plane & a in E2 & b in E2 & c in E2 holds
E1 = E2
let E1, E2 be Subset of S; :: thesis: ( E1 is_plane & a in E1 & b in E1 & c in E1 & E2 is_plane & a in E2 & b in E2 & c in E2 implies E1 = E2 )
assume that
A2: ( E1 is_plane & a in E1 & b in E1 & c in E1 ) and
A3: ( E2 is_plane & a in E2 & b in E2 & c in E2 ) ; :: thesis: E1 = E2
thus E1 = Plane (a,b,c) by A1, A2, Th47
.= E2 by A1, A3, Th47 ; :: thesis: verum