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
proof
assume M // N ; :: thesis: contradiction
then A // N by A5, AFF_1:44;
hence contradiction by A3, A6, AFF_1:44; :: thesis: verum
end;
hence Y '||' X by A1, A4, A5, A6, Th55; :: thesis: verum