let T be non empty TopSpace; :: thesis: for a, b being Element of (Open_Domains_Lattice T)
for A, B being Element of Open_Domains_of T st a = A & b = B holds
( a [= b iff A c= B )
let a, b be Element of (Open_Domains_Lattice T); :: thesis: for A, B being Element of Open_Domains_of T st a = A & b = B holds
( a [= b iff A c= B )
let A, B be Element of Open_Domains_of T; :: thesis: ( a = A & b = B implies ( a [= b iff A c= B ) )
reconsider A1 = A as Subset of T ;
assume that
A1: a = A and
A2: b = B ; :: thesis: ( a [= b iff A c= B )
A in Open_Domains_of T ;
then A in { C where C is Subset of T : C is open_condensed } by TDLAT_1:def 9;
then ex Q being Subset of T st
( Q = A & Q is open_condensed ) ;
then A3: A1 is open by TOPS_1:67;
thus ( a [= b implies A c= B ) :: thesis: ( A c= B implies a [= b )

proof

assume a [= b ; :: thesis: A c= B
then a "\/" b = b by LATTICES:def 3;
then Int (Cl (A \/ B)) = B by A1, A2, Th103;
hence A c= B by A3, Th4; :: thesis: verum

end;

B in Open_Domains_of T ;
then B in { C where C is Subset of T : C is open_condensed } by TDLAT_1:def 9;
then A4: ex P being Subset of T st
( P = B & P is open_condensed ) ;
thus ( A c= B implies a [= b ) :: thesis: verum

proof

assume A c= B ; :: thesis: a [= b
then Int (Cl (A \/ B)) = B by A4, Th63;
then a "\/" b = b by A1, A2, Th103;
hence a [= b by LATTICES:def 3; :: thesis: verum

end;