let AS be AffinSpace; :: thesis: for X, Y being Subset of AS st X is being_plane & Y is being_plane & X '||' Y holds

Y '||' X

let X, Y be Subset of AS; :: thesis: ( X is being_plane & Y is being_plane & X '||' Y implies Y '||' X )

assume that

A1: ( X is being_plane & Y is being_plane ) and

A2: X '||' Y ; :: thesis: Y '||' X

consider A, P, M, N being Subset of AS such that

A3: not A // P and

A4: ( A c= X & P c= X & M c= Y & N c= Y ) and

A5: ( A // M or M // A ) and

A6: ( P // N or N // P ) by A1, A2, Th55;

not M // N

Y '||' X

let X, Y be Subset of AS; :: thesis: ( X is being_plane & Y is being_plane & X '||' Y implies Y '||' X )

assume that

A1: ( X is being_plane & Y is being_plane ) and

A2: X '||' Y ; :: thesis: Y '||' X

consider A, P, M, N being Subset of AS such that

A3: not A // P and

A4: ( A c= X & P c= X & M c= Y & N c= Y ) and

A5: ( A // M or M // A ) and

A6: ( P // N or N // P ) by A1, A2, Th55;

not M // N

proof

hence
Y '||' X
by A1, A4, A5, A6, Th55; :: thesis: verum
assume
M // N
; :: thesis: contradiction

then A // N by A5, AFF_1:44;

hence contradiction by A3, A6, AFF_1:44; :: thesis: verum

end;then A // N by A5, AFF_1:44;

hence contradiction by A3, A6, AFF_1:44; :: thesis: verum