set AFP = AfPlanes AS;
set AFP2 = [:(AfPlanes AS),(AfPlanes AS):];
set R1 = { [X,Y] where X, Y is Subset of AS : ( X is being_plane & Y is being_plane & X '||' Y ) } ;

now :: thesis: for x being object st x in { [X,Y] where X, Y is Subset of AS : ( X is being_plane & Y is being_plane & X '||' Y ) } holds
x in [:(AfPlanes AS),(AfPlanes AS):]

let x be object ; :: thesis: ( x in { [X,Y] where X, Y is Subset of AS : ( X is being_plane & Y is being_plane & X '||' Y ) } implies x in [:(AfPlanes AS),(AfPlanes AS):] )
assume x in { [X,Y] where X, Y is Subset of AS : ( X is being_plane & Y is being_plane & X '||' Y ) } ; :: thesis: x in [:(AfPlanes AS),(AfPlanes AS):]
then consider X, Y being Subset of AS such that
A1: x = [X,Y] and
A2: X is being_plane and
A3: Y is being_plane and
X '||' Y ;
A4: Y in AfPlanes AS by A3;
X in AfPlanes AS by A2;
hence x in [:(AfPlanes AS),(AfPlanes AS):] by A1, A4, ZFMISC_1:def 2; :: thesis: verum

end;

then reconsider R2 = { [X,Y] where X, Y is Subset of AS : ( X is being_plane & Y is being_plane & X '||' Y ) } as Relation of (AfPlanes AS),(AfPlanes AS) by TARSKI:def 3;

now :: thesis: for x being object st x in AfPlanes AS holds
[x,x] in R2

let x be object ; :: thesis: ( x in AfPlanes AS implies [x,x] in R2 )
assume x in AfPlanes AS ; :: thesis: [x,x] in R2
then consider X being Subset of AS such that
A5: x = X and
A6: X is being_plane ;
X '||' X by A6, AFF_4:57;
hence [x,x] in R2 by A5, A6; :: thesis: verum

end;

then A7: R2 is_reflexive_in AfPlanes AS by RELAT_2:def 1;
then A8: field R2 = AfPlanes AS by ORDERS_1:13;
A9: for X, Y being Subset of AS st X is being_plane & Y is being_plane holds
( [X,Y] in { [X,Y] where X, Y is Subset of AS : ( X is being_plane & Y is being_plane & X '||' Y ) } iff X '||' Y )

proof

let X, Y be Subset of AS; :: thesis: ( X is being_plane & Y is being_plane implies ( [X,Y] in { [X,Y] where X, Y is Subset of AS : ( X is being_plane & Y is being_plane & X '||' Y ) } iff X '||' Y ) )
assume that
A10: X is being_plane and
A11: Y is being_plane ; :: thesis: ( [X,Y] in { [X,Y] where X, Y is Subset of AS : ( X is being_plane & Y is being_plane & X '||' Y ) } iff X '||' Y )

now :: thesis: ( [X,Y] in { [X,Y] where X, Y is Subset of AS : ( X is being_plane & Y is being_plane & X '||' Y ) } implies X '||' Y )

assume [X,Y] in { [X,Y] where X, Y is Subset of AS : ( X is being_plane & Y is being_plane & X '||' Y ) } ; :: thesis: X '||' Y
then consider X9, Y9 being Subset of AS such that
A12: [X,Y] = [X9,Y9] and
X9 is being_plane and
Y9 is being_plane and
A13: X9 '||' Y9 ;
X = X9 by A12, XTUPLE_0:1;
hence X '||' Y by A12, A13, XTUPLE_0:1; :: thesis: verum

end;

hence ( [X,Y] in { [X,Y] where X, Y is Subset of AS : ( X is being_plane & Y is being_plane & X '||' Y ) } iff X '||' Y ) by A10, A11; :: thesis: verum

end;

now :: thesis: for x, y, z being object st x in AfPlanes AS & y in AfPlanes AS & z in AfPlanes AS & [x,y] in R2 & [y,z] in R2 holds
[x,z] in R2

let x, y, z be object ; :: thesis: ( x in AfPlanes AS & y in AfPlanes AS & z in AfPlanes AS & [x,y] in R2 & [y,z] in R2 implies [x,z] in R2 )
assume that
A14: x in AfPlanes AS and
A15: y in AfPlanes AS and
A16: z in AfPlanes AS and
A17: [x,y] in R2 and
A18: [y,z] in R2 ; :: thesis: [x,z] in R2
consider X being Subset of AS such that
A19: x = X and
A20: X is being_plane by A14;
consider Y being Subset of AS such that
A21: y = Y and
A22: Y is being_plane by A15;
consider Z being Subset of AS such that
A23: z = Z and
A24: Z is being_plane by A16;
A25: Y '||' Z by A9, A18, A21, A22, A23, A24;
X '||' Y by A9, A17, A19, A20, A21, A22;
then X '||' Z by A20, A22, A24, A25, AFF_4:61;
hence [x,z] in R2 by A19, A20, A23, A24; :: thesis: verum

end;

then A26: R2 is_transitive_in AfPlanes AS by RELAT_2:def 8;

now :: thesis: for x, y being object st x in AfPlanes AS & y in AfPlanes AS & [x,y] in R2 holds
[y,x] in R2

let x, y be object ; :: thesis: ( x in AfPlanes AS & y in AfPlanes AS & [x,y] in R2 implies [y,x] in R2 )
assume that
A27: x in AfPlanes AS and
A28: y in AfPlanes AS and
A29: [x,y] in R2 ; :: thesis: [y,x] in R2
consider X being Subset of AS such that
A30: x = X and
A31: X is being_plane by A27;
consider Y being Subset of AS such that
A32: y = Y and
A33: Y is being_plane by A28;
X '||' Y by A9, A29, A30, A31, A32, A33;
then Y '||' X by A31, A33, AFF_4:58;
hence [y,x] in R2 by A30, A31, A32, A33; :: thesis: verum

end;

then A34: R2 is_symmetric_in AfPlanes AS by RELAT_2:def 3;
dom R2 = AfPlanes AS by A7, ORDERS_1:13;
hence { [X,Y] where X, Y is Subset of AS : ( X is being_plane & Y is being_plane & X '||' Y ) } is Equivalence_Relation of (AfPlanes AS) by A8, A34, A26, PARTFUN1:def 2, RELAT_2:def 11, RELAT_2:def 16; :: thesis: verum