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