set AFL = AfLines AS;
set AFL2 = [:(AfLines AS),(AfLines AS):];
set R1 = { [X,Y] where X, Y is Subset of AS : ( X is being_line & Y is being_line & X '||' Y ) } ;

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

let x be object ; :: thesis: ( x in { [X,Y] where X, Y is Subset of AS : ( X is being_line & Y is being_line & X '||' Y ) } implies x in [:(AfLines AS),(AfLines AS):] )
assume x in { [X,Y] where X, Y is Subset of AS : ( X is being_line & Y is being_line & X '||' Y ) } ; :: thesis: x in [:(AfLines AS),(AfLines AS):]
then consider X, Y being Subset of AS such that
A1: x = [X,Y] and
A2: X is being_line and
A3: Y is being_line and
X '||' Y ;
A4: Y in AfLines AS by A3;
X in AfLines AS by A2;
hence x in [:(AfLines AS),(AfLines 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_line & Y is being_line & X '||' Y ) } as Relation of (AfLines AS),(AfLines AS) by TARSKI:def 3;

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

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

end;

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

proof

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

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

assume [X,Y] in { [X,Y] where X, Y is Subset of AS : ( X is being_line & Y is being_line & X '||' Y ) } ; :: thesis: X '||' Y
then consider X9, Y9 being Subset of AS such that
A12: [X,Y] = [X9,Y9] and
X9 is being_line and
Y9 is being_line 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_line & Y is being_line & X '||' Y ) } iff X '||' Y ) by A10, A11; :: thesis: verum

end;

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

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

end;

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

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

let x, y be object ; :: thesis: ( x in AfLines AS & y in AfLines AS & [x,y] in R2 implies [y,x] in R2 )
assume that
A27: x in AfLines AS and
A28: y in AfLines 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_line by A27;
consider Y being Subset of AS such that
A32: y = Y and
A33: Y is being_line by A28;
X '||' Y by A9, A29, A30, A31, A32, A33;
then X // Y by A31, A33, AFF_4:40;
then Y '||' X by A31, A33, AFF_4:40;
hence [y,x] in R2 by A30, A31, A32, A33; :: thesis: verum

end;

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