let A, B be set ; :: thesis: for X1, X2 being Subset of A
for R being Subset of [:A,B:] st X1 c= X2 holds
R .:^ X2 c= R .:^ X1
let X1, X2 be Subset of A; :: thesis: for R being Subset of [:A,B:] st X1 c= X2 holds
R .:^ X2 c= R .:^ X1
let R be Subset of [:A,B:]; :: thesis: ( X1 c= X2 implies R .:^ X2 c= R .:^ X1 )
assume X1 c= X2 ; :: thesis: R .:^ X2 c= R .:^ X1
then A1: {_{X1}_} c= {_{X2}_} by Th6;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in R .:^ X2 or y in R .:^ X1 )
assume A2: y in R .:^ X2 ; :: thesis: y in R .:^ X1
per cases ( (.: R) .: {_{X2}_} = {} or (.: R) .: {_{X2}_} <> {} ) ;
suppose A3: (.: R) .: {_{X2}_} = {} ; :: thesis: y in R .:^ X1
per cases ( (.: R) .: {_{X1}_} = {} or (.: R) .: {_{X1}_} <> {} ) ;
suppose A4: (.: R) .: {_{X1}_} <> {} ; :: thesis: y in R .:^ X1
for Y being set st Y in (.: R) .: {_{X1}_} holds
y in Y
proof
let Y be set ; :: thesis: ( Y in (.: R) .: {_{X1}_} implies y in Y )
assume Y in (.: R) .: {_{X1}_} ; :: thesis: y in Y
then ex x being object st
( [x,Y] in .: R & x in {_{X1}_} ) by RELAT_1:def 13;
hence y in Y by A1, A3, RELAT_1:def 13; :: thesis: verum
end;
then y in meet ((.: R) .: {_{X1}_}) by A4, SETFAM_1:def 1;
hence y in R .:^ X1 by A4, SETFAM_1:def 9; :: thesis: verum
end;
end;
end;
suppose (.: R) .: {_{X2}_} <> {} ; :: thesis: y in R .:^ X1
then A5: y in meet ((.: R) .: {_{X2}_}) by A2, SETFAM_1:def 9;
end;
end;