let L be lower-bounded continuous sup-Semilattice; :: thesis: for B being with_bottom CLbasis of L holds the carrier of (CompactSublatt (InclPoset (Ids ()))) = { () where b is Element of () : verum }
let B be with_bottom CLbasis of L; :: thesis: the carrier of (CompactSublatt (InclPoset (Ids ()))) = { () where b is Element of () : verum }
thus the carrier of (CompactSublatt (InclPoset (Ids ()))) c= { () where b is Element of () : verum } :: according to XBOOLE_0:def 10 :: thesis: { () where b is Element of () : verum } c= the carrier of (CompactSublatt (InclPoset (Ids ())))
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of (CompactSublatt (InclPoset (Ids ()))) or x in { () where b is Element of () : verum } )
assume A1: x in the carrier of (CompactSublatt (InclPoset (Ids ()))) ; :: thesis: x in { () where b is Element of () : verum }
the carrier of (CompactSublatt (InclPoset (Ids ()))) c= the carrier of (InclPoset (Ids ())) by YELLOW_0:def 13;
then reconsider x1 = x as Element of (InclPoset (Ids ())) by A1;
x1 is compact by ;
then ex b being Element of () st x1 = downarrow b by WAYBEL13:12;
hence x in { () where b is Element of () : verum } ; :: thesis: verum
end;
thus { (downarrow b) where b is Element of () : verum } c= the carrier of (CompactSublatt (InclPoset (Ids ()))) :: thesis: verum
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { () where b is Element of () : verum } or x in the carrier of (CompactSublatt (InclPoset (Ids ()))) )
assume x in { () where b is Element of () : verum } ; :: thesis: x in the carrier of (CompactSublatt (InclPoset (Ids ())))
then A2: ex b being Element of () st x = downarrow b ;
then reconsider x1 = x as Element of (InclPoset (Ids ())) by YELLOW_2:41;
x1 is compact by ;
hence x in the carrier of (CompactSublatt (InclPoset (Ids ()))) by WAYBEL_8:def 1; :: thesis: verum
end;