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