let AS be AffinSpace; :: thesis: for K, M, P being Subset of AS st K // M holds

Plane (K,P) = Plane (M,P)

let K, M, P be Subset of AS; :: thesis: ( K // M implies Plane (K,P) = Plane (M,P) )

assume A1: K // M ; :: thesis: Plane (K,P) = Plane (M,P)

Plane (K,P) = Plane (M,P)

let K, M, P be Subset of AS; :: thesis: ( K // M implies Plane (K,P) = Plane (M,P) )

assume A1: K // M ; :: thesis: Plane (K,P) = Plane (M,P)

now :: thesis: for x being object holds

( x in Plane (K,P) iff x in Plane (M,P) )

hence
Plane (K,P) = Plane (M,P)
by TARSKI:2; :: thesis: verum( x in Plane (K,P) iff x in Plane (M,P) )

let x be object ; :: thesis: ( x in Plane (K,P) iff x in Plane (M,P) )

end;A2: now :: thesis: ( x in Plane (M,P) implies x in Plane (K,P) )

assume
x in Plane (M,P)
; :: thesis: x in Plane (K,P)

then consider a being Element of AS such that

A3: x = a and

A4: ex b being Element of AS st

( a,b // M & b in P ) ;

consider b being Element of AS such that

A5: a,b // M and

A6: b in P by A4;

a,b // K by A1, A5, AFF_1:43;

hence x in Plane (K,P) by A3, A6; :: thesis: verum

end;then consider a being Element of AS such that

A3: x = a and

A4: ex b being Element of AS st

( a,b // M & b in P ) ;

consider b being Element of AS such that

A5: a,b // M and

A6: b in P by A4;

a,b // K by A1, A5, AFF_1:43;

hence x in Plane (K,P) by A3, A6; :: thesis: verum

now :: thesis: ( x in Plane (K,P) implies x in Plane (M,P) )

hence
( x in Plane (K,P) iff x in Plane (M,P) )
by A2; :: thesis: verumassume
x in Plane (K,P)
; :: thesis: x in Plane (M,P)

then consider a being Element of AS such that

A7: x = a and

A8: ex b being Element of AS st

( a,b // K & b in P ) ;

consider b being Element of AS such that

A9: a,b // K and

A10: b in P by A8;

a,b // M by A1, A9, AFF_1:43;

hence x in Plane (M,P) by A7, A10; :: thesis: verum

end;then consider a being Element of AS such that

A7: x = a and

A8: ex b being Element of AS st

( a,b // K & b in P ) ;

consider b being Element of AS such that

A9: a,b // K and

A10: b in P by A8;

a,b // M by A1, A9, AFF_1:43;

hence x in Plane (M,P) by A7, A10; :: thesis: verum