let X, Y be Subset of CQC-WFF; :: thesis: for p being Element of CQC-WFF st X |- p & X c= Y holds
Y |- p
let p be Element of CQC-WFF ; :: thesis: ( X |- p & X c= Y implies Y |- p )
assume that
A1: X |- p and
A2: X c= Y ; :: thesis: Y |- p
consider f being FinSequence of CQC-WFF such that
A3: rng f c= X and
A4: |- f ^ <*p*> by A1, HENMODEL:def 1;
rng f c= Y by A2, A3, XBOOLE_1:1;
hence Y |- p by A4, HENMODEL:def 1; :: thesis: verum