let P, R be Relation; :: thesis: for x being set holds
( x in ["P,R"] iff ( [((x `1 ) `1 ),((x `2 ) `1 )] in P & [((x `1 ) `2 ),((x `2 ) `2 )] in R & ex a, b being set st x = [a,b] & ex c, d being set st x `1 = [c,d] & ex e, f being set st x `2 = [e,f] ) )
let x be set ; :: thesis: ( x in ["P,R"] iff ( [((x `1 ) `1 ),((x `2 ) `1 )] in P & [((x `1 ) `2 ),((x `2 ) `2 )] in R & ex a, b being set st x = [a,b] & ex c, d being set st x `1 = [c,d] & ex e, f being set st x `2 = [e,f] ) )
hereby :: thesis: ( [((x `1 ) `1 ),((x `2 ) `1 )] in P & [((x `1 ) `2 ),((x `2 ) `2 )] in R & ex a, b being set st x = [a,b] & ex c, d being set st x `1 = [c,d] & ex e, f being set st x `2 = [e,f] implies x in ["P,R"] )
assume A1:
x in ["P,R"]
;
:: thesis: ( [((x `1 ) `1 ),((x `2 ) `1 )] in P & [((x `1 ) `2 ),((x `2 ) `2 )] in R & ex a, b being set st x = [a,b] & ex c, d being set st x `1 = [c,d] & ex e, f being set st x `2 = [e,f] )then consider y,
z being
set such that A2:
x = [y,z]
by RELAT_1:def 1;
consider p,
q,
s,
t being
set such that A3:
(
y = [p,q] &
z = [s,t] &
[p,s] in P &
[q,t] in R )
by A1, A2, Def1;
(
(x `1 ) `1 = p &
(x `1 ) `2 = q &
(x `2 ) `1 = s &
(x `2 ) `2 = t )
by A2, A3, Lm1;
hence
(
[((x `1 ) `1 ),((x `2 ) `1 )] in P &
[((x `1 ) `2 ),((x `2 ) `2 )] in R )
by A3;
:: thesis: ( ex a, b being set st x = [a,b] & ex c, d being set st x `1 = [c,d] & ex e, f being set st x `2 = [e,f] )thus
ex
a,
b being
set st
x = [a,b]
by A2;
:: thesis: ( ex c, d being set st x `1 = [c,d] & ex e, f being set st x `2 = [e,f] )
x `1 = [p,q]
by A2, A3, MCART_1:7;
hence
ex
c,
d being
set st
x `1 = [c,d]
;
:: thesis: ex e, f being set st x `2 = [e,f]
x `2 = [s,t]
by A2, A3, MCART_1:7;
hence
ex
e,
f being
set st
x `2 = [e,f]
;
:: thesis: verum
end;
assume that
A4:
( [((x `1 ) `1 ),((x `2 ) `1 )] in P & [((x `1 ) `2 ),((x `2 ) `2 )] in R )
and
A5:
( ex a, b being set st x = [a,b] & ex c, d being set st x `1 = [c,d] & ex e, f being set st x `2 = [e,f] )
; :: thesis: x in ["P,R"]
consider a, b being set such that
A6:
x = [a,b]
by A5;
consider c, d being set such that
A7:
x `1 = [c,d]
by A5;
consider e, f being set such that
A8:
x `2 = [e,f]
by A5;
A9:
( a = [c,d] & b = [e,f] )
by A6, A7, A8, MCART_1:7;
( [c,((x `2 ) `1 )] in P & [d,((x `2 ) `2 )] in R )
by A4, A7, MCART_1:7;
then
( [c,e] in P & [d,f] in R )
by A8, MCART_1:7;
hence
x in ["P,R"]
by A6, A9, Def1; :: thesis: verum