let AS be AffinSpace; :: thesis: for a, b, c being Element of AS
for X, Y being Subset of AS st X is being_plane & Y is being_plane & a in X & b in X & c in X & a in Y & b in Y & c in Y & not LIN a,b,c holds
X = Y
let a, b, c be Element of AS; :: thesis: for X, Y being Subset of AS st X is being_plane & Y is being_plane & a in X & b in X & c in X & a in Y & b in Y & c in Y & not LIN a,b,c holds
X = Y
let X, Y be Subset of AS; :: thesis: ( X is being_plane & Y is being_plane & a in X & b in X & c in X & a in Y & b in Y & c in Y & not LIN a,b,c implies X = Y )
assume that
A1: ( X is being_plane & Y is being_plane ) and
A2: ( a in X & b in X ) and
A3: c in X and
A4: ( a in Y & b in Y ) and
A5: c in Y and
A6: not LIN a,b,c ; :: thesis: X = Y
assume A7: not X = Y ; :: thesis: contradiction
a <> b by A6, AFF_1:7;
then A8: X /\ Y is being_line by A1, A2, A4, A7, Th24;
A9: c in X /\ Y by A3, A5, XBOOLE_0:def 4;
( a in X /\ Y & b in X /\ Y ) by A2, A4, XBOOLE_0:def 4;
hence contradiction by A6, A8, A9, AFF_1:21; :: thesis: verum