let GX be TopStruct ; :: thesis: for T being Subset of GX holds Fr T = ((Cl (T `)) /\ T) \/ ((Cl T) \ T)
let T be Subset of GX; :: thesis: Fr T = ((Cl (T `)) /\ T) \/ ((Cl T) \ T)
for x being object holds
( x in Fr T iff x in ((Cl (T `)) /\ T) \/ ((Cl T) \ T) )
proof
let x be object ; :: thesis: ( x in Fr T iff x in ((Cl (T `)) /\ T) \/ ((Cl T) \ T) )
A1: T ` c= Cl (T `) by PRE_TOPC:18;
thus ( x in Fr T implies x in ((Cl (T `)) /\ T) \/ ((Cl T) \ T) ) :: thesis: ( x in ((Cl (T `)) /\ T) \/ ((Cl T) \ T) implies x in Fr T )
proof
assume A2: x in Fr T ; :: thesis: x in ((Cl (T `)) /\ T) \/ ((Cl T) \ T)
then reconsider x99 = x as Point of GX ;
( ( x99 in Cl T & x99 in Cl (T `) & x99 in T ) or ( x99 in Cl T & x99 in Cl (T `) & x99 in T ` ) ) by A2, SUBSET_1:29, XBOOLE_0:def 4;
then ( x99 in (Cl (T `)) /\ T or ( not x99 in T & x99 in Cl T ) ) by XBOOLE_0:def 4;
then ( x99 in (Cl (T `)) /\ T or x99 in (Cl T) \ T ) by XBOOLE_0:def 5;
hence x in ((Cl (T `)) /\ T) \/ ((Cl T) \ T) by XBOOLE_0:def 3; :: thesis: verum
end;
A3: T c= Cl T by PRE_TOPC:18;
thus ( x in ((Cl (T `)) /\ T) \/ ((Cl T) \ T) implies x in Fr T ) :: thesis: verum
proof
assume A4: x in ((Cl (T `)) /\ T) \/ ((Cl T) \ T) ; :: thesis: x in Fr T
then reconsider x99 = x as Point of GX ;
( x99 in (Cl (T `)) /\ T or x99 in (Cl T) \ T ) by A4, XBOOLE_0:def 3;
then ( ( x99 in Cl (T `) & x99 in T ) or ( x99 in Cl T & not x99 in T ) ) by XBOOLE_0:def 4, XBOOLE_0:def 5;
then ( ( x99 in Cl (T `) & x99 in T ) or ( x99 in Cl T & x99 in T ` ) ) by SUBSET_1:29;
hence x in Fr T by A3, A1, XBOOLE_0:def 4; :: thesis: verum
end;
end;
hence Fr T = ((Cl (T `)) /\ T) \/ ((Cl T) \ T) by TARSKI:2; :: thesis: verum