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 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 ;
( 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 ) }
;
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;
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;
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;
( 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
;
( [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 )
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;
verum
end;
now 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 R2let x,
y,
z be
object ;
( 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
;
[x,z] in R2consider 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;
verum end;
then A26:
R2 is_transitive_in AfLines AS
by RELAT_2:def 8;
now for x, y being object st x in AfLines AS & y in AfLines AS & [x,y] in R2 holds
[y,x] in R2let x,
y be
object ;
( 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
;
[y,x] in R2consider 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;
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; verum