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 (.: R) .: {_{X1}_} = {} ; :: thesis: y in R .:^ X1

then Intersect ((.: R) .: {_{X1}_}) = B by SETFAM_1:def 9;
hence y in R .:^ X1 by A2; :: thesis: verum

end;

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;

per cases ( (.: R) .: {_{X1}_} = {} or (.: R) .: {_{X1}_} <> {} ) ;

suppose (.: R) .: {_{X1}_} = {} ; :: thesis: y in R .:^ X1

then Intersect ((.: R) .: {_{X1}_}) = B by SETFAM_1:def 9;
hence y in R .:^ X1 by A2; :: thesis: verum

end;

suppose A6: (.: R) .: {_{X1}_} <> {} ; :: thesis: y in R .:^ X1

(.: R) .: {_{X1}_} c= (.: R) .: {_{X2}_} by A1, RELAT_1:123;
then meet ((.: R) .: {_{X2}_}) c= meet ((.: R) .: {_{X1}_}) by A6, SETFAM_1:6;
then y in meet ((.: R) .: {_{X1}_}) by A5;
hence y in R .:^ X1 by A6, SETFAM_1:def 9; :: thesis: verum

end;

end;

end;

end;