let C be set ; :: thesis: ( C is subset-closed implies C is multiplicative )
assume A1: C is subset-closed ; :: thesis: C is multiplicative
let x, y be set ; :: according to FINSUB_1:def 2 :: thesis: ( not x in C or not y in C or x /\ y in C )
x /\ y c= x by XBOOLE_1:17;
hence ( not x in C or not y in C or x /\ y in C ) by A1; :: thesis: verum