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 set ; :: 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 10;
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 consider x being set such that
A5: ( [x,Y] in .: R & x in {_{X1}_} ) by RELAT_1:def 13;
thus y in Y by A1, A3, A5, 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 10; :: thesis: verum

end;

end;

end;

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

then A6: y in meet ((.: R) .: {_{X2}_}) by A2, SETFAM_1:def 10;

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

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

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

end;

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

(.: R) .: {_{X1}_} c= (.: R) .: {_{X2}_} by A1, RELAT_1:156;
then meet ((.: R) .: {_{X2}_}) c= meet ((.: R) .: {_{X1}_}) by A7, SETFAM_1:7;
then y in meet ((.: R) .: {_{X1}_}) by A6;
hence y in R .:^ X1 by A7, SETFAM_1:def 10; :: thesis: verum

end;

end;

end;

end;