let N be non empty reflexive RelStr ; :: thesis: for A, J being Subset of N st A c= J holds
A ^0 c= J ^0
let A, J be Subset of N; :: thesis: ( A c= J implies A ^0 c= J ^0 )
assume A1: A c= J ; :: thesis: A ^0 c= J ^0
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in A ^0 or a in J ^0 )
assume a in A ^0 ; :: thesis: a in J ^0
then consider u being Element of N such that
A2: a = u and
A3: for D being non empty directed Subset of N st u <= sup D holds
A meets D ;
for D being non empty directed Subset of N st u <= sup D holds
J meets D by A1, A3, XBOOLE_1:63;
hence a in J ^0 by A2; :: thesis: verum