let P, R be Relation; :: thesis: for x being object 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 object st x = [a,b] & ex c, d being object st x `1 = [c,d] & ex e, f being object st x `2 = [e,f] ) )
let x be object ; :: 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 object st x = [a,b] & ex c, d being object st x `1 = [c,d] & ex e, f being object 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 object st x = [a,b] & ex c, d being object st x `1 = [c,d] & ex e, f being object 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 object st x = [a,b] & ex c, d being object st x `1 = [c,d] & ex e, f being object st x `2 = [e,f] )
then consider y, z being object such that
A2: x = [y,z] by RELAT_1:def 1;
consider p, q, s, t being object such that
A3: y = [p,q] and
A4: z = [s,t] and
A5: ( [p,s] in P & [q,t] in R ) by A1, A2, Def1;
( (x `1) `1 = p & (x `1) `2 = q ) by A2, A3;
hence ( [((x `1) `1),((x `2) `1)] in P & [((x `1) `2),((x `2) `2)] in R ) by A2, A4, A5; :: thesis: ( ex a, b being object st x = [a,b] & ex c, d being object st x `1 = [c,d] & ex e, f being object st x `2 = [e,f] )
thus ex a, b being object st x = [a,b] by A2; :: thesis: ( ex c, d being object st x `1 = [c,d] & ex e, f being object st x `2 = [e,f] )
thus ex c, d being object st x `1 = [c,d] by A2, A3; :: thesis: ex e, f being object st x `2 = [e,f]
thus ex e, f being object st x `2 = [e,f] by A2, A4; :: thesis: verum
end;
assume that
A6: [((x `1) `1),((x `2) `1)] in P and
A7: [((x `1) `2),((x `2) `2)] in R ; :: thesis: ( for a, b being object holds not x = [a,b] or for c, d being object holds not x `1 = [c,d] or for e, f being object holds not x `2 = [e,f] or x in ["P,R"] )
given a, b being object such that A8: x = [a,b] ; :: thesis: ( for c, d being object holds not x `1 = [c,d] or for e, f being object holds not x `2 = [e,f] or x in ["P,R"] )
given c, d being object such that A9: x `1 = [c,d] ; :: thesis: ( for e, f being object holds not x `2 = [e,f] or x in ["P,R"] )
given e, f being object such that A10: x `2 = [e,f] ; :: thesis: x in ["P,R"]
[c,((x `2) `1)] in P by A6, A9;
then A11: [c,e] in P by A10;
[d,((x `2) `2)] in R by A7, A9;
then A12: [d,f] in R by A10;
A13: b = [e,f] by A8, A10;
a = [c,d] by A8, A9;
hence x in ["P,R"] by A8, A13, A11, A12, Def1; :: thesis: verum