set S = { [F_{3}(x),F_{4}(x)] where x is Element of F_{1}() : P_{1}[x] } ;

{ [F_{3}(x),F_{4}(x)] where x is Element of F_{1}() : P_{1}[x] } is Relation-like
_{3}(x),F_{4}(x)] where x is Element of F_{1}() : P_{1}[x] } as Relation ;

A2: for x, y being object st [y,x] in F_{2}() holds

[x,y] in S9

[y,x] in F_{2}()
_{2}() ~ = { [F_{3}(x),F_{4}(x)] where x is Element of F_{1}() : P_{1}[x] }
by A2, RELAT_1:def 7; :: thesis: verum

{ [F

proof

then reconsider S9 = { [F
let x be object ; :: according to RELAT_1:def 1 :: thesis: ( not x in { [F_{3}(x),F_{4}(x)] where x is Element of F_{1}() : P_{1}[x] } or ex b_{1}, b_{2} being object st x = [b_{1},b_{2}] )

assume x in { [F_{3}(x),F_{4}(x)] where x is Element of F_{1}() : P_{1}[x] }
; :: thesis: ex b_{1}, b_{2} being object st x = [b_{1},b_{2}]

then ex y being Element of F_{1}() st

( x = [F_{3}(y),F_{4}(y)] & P_{1}[y] )
;

hence ex b_{1}, b_{2} being object st x = [b_{1},b_{2}]
; :: thesis: verum

end;assume x in { [F

then ex y being Element of F

( x = [F

hence ex b

A2: for x, y being object st [y,x] in F

[x,y] in S9

proof

for x, y being object st [x,y] in S9 holds
let x, y be object ; :: thesis: ( [y,x] in F_{2}() implies [x,y] in S9 )

assume [y,x] in F_{2}()
; :: thesis: [x,y] in S9

then consider z being Element of F_{1}() such that

A3: [y,x] = [F_{4}(z),F_{3}(z)]
and

A4: P_{1}[z]
by A1;

( y = F_{4}(z) & x = F_{3}(z) )
by A3, XTUPLE_0:1;

hence [x,y] in S9 by A4; :: thesis: verum

end;assume [y,x] in F

then consider z being Element of F

A3: [y,x] = [F

A4: P

( y = F

hence [x,y] in S9 by A4; :: thesis: verum

[y,x] in F

proof

hence
F
let x, y be object ; :: thesis: ( [x,y] in S9 implies [y,x] in F_{2}() )

assume [x,y] in S9 ; :: thesis: [y,x] in F_{2}()

then consider z being Element of F_{1}() such that

A5: [x,y] = [F_{3}(z),F_{4}(z)]
and

A6: P_{1}[z]
;

( x = F_{3}(z) & y = F_{4}(z) )
by A5, XTUPLE_0:1;

hence [y,x] in F_{2}()
by A1, A6; :: thesis: verum

end;assume [x,y] in S9 ; :: thesis: [y,x] in F

then consider z being Element of F

A5: [x,y] = [F

A6: P

( x = F

hence [y,x] in F